\begin{tabbing}
$\forall$$A$:Type, $r$:($A$$\rightarrow$$A$$\rightarrow\mathbb{B}$), $L$:$A$ List.
\\[0ex]($\forall$$a$:$A$. $r$($a$,$a$))
\\[0ex]$\Rightarrow$ $\neg$null($L$)
\\[0ex]$\Rightarrow$ (\=$\exists$$L_{1}$, $L_{2}$:$A$ List.\+
\\[0ex]$L$ $=$ ($L_{1}$ @ $L_{2}$) \& $\neg$null($L_{2}$) \& ($\forall$$b$$\in$$L_{2}$. $r$($b$,last($L$)))
\\[0ex]\& ($\neg$null($L_{1}$) $\Rightarrow$ $\neg$$r$(last($L_{1}$),last($L$))))
\-
\end{tabbing}